HOL Light
定理証明支援系
OCaml
で書かれている。
HOL
のLightバージョン...?
OCaml
が動かすのに必要
HOL Light
HOL Light: an overview
GitHub:
jrh13/hol-light: The HOL Light theorem prover
HOL Lightのインストール
HOL Lightとは? - ATPとCASのこと
関連
『定理証明支援系 Coq 入門 SSReflect 中心』
#定理証明支援系